package ResK.calculi

import scala.util.parsing.combinator._
import scala.collection.mutable._
import java.io.FileReader
import ResK.calculi.resolution._

object ProofParser extends JavaTokenParsers with RegexParsers {
  private var spmap = new HashMap[String,Proof]
  private var atmap = new HashMap[String,Int]
  private var nextat = 0
  private var root : Proof = null

  def proof: Parser[Any] = rep(line)
  def line: Parser[(Any,Proof)] = proofName ~ "=" ~ subproof ^^ {
    case ~(~(name,_),p) => {
        spmap += (name.asInstanceOf[String] -> p)
        if (p.clause.isEmpty) root = p
        (name,p)
      }
  }
  def subproof: Parser[Proof] = (input | resolvent | leftChain | proofName) ^^ {
    case p: Proof => p
    case name: String => spmap(name)
  }
  def input: Parser[Proof] = "{" ~> repsep(literal,",") <~ "}" ^^ {
    list => new ResK.calculi.resolution.Input(list.toSet[Literal])
  }
  def resolvent: Parser[Proof] = "(" ~> subproof ~ "." ~ subproof <~ ")" ^^ {
    case ~(~(left,_),right) => new Resolvent(left,right)
  }
  def leftChain: Parser[Proof] = "L(" ~> repsep(subproof, ".") <~ ")" ^^ {
    list => (list.head /: list.tail)(
      (p1,p2) => new Resolvent(p1,p2)
    )
  }

  def literal: Parser[Literal] = opt("-")~atom ^^ {
    case ~(Some(_),a) => L(a, false)
    case ~(None,a) => L(a, true)
  }

  def proofName: Parser[String] = """\w+""".r
  def atom: Parser[Atom] = """\w+""".r ^^ {s =>
    if (atmap contains s) atmap(s)
    else {
      atmap += (s -> nextat)
      nextat += 1
      nextat - 1
    }
  }

  def reset() : Unit = {
    spmap = new HashMap[String,Proof]
    atmap = new HashMap[String,Int]
    nextat = 0
    root = null
  }

  def getProofFromFile(filename: String) = {
    reset()
    parse(proof, new FileReader(filename))
    root
  }
}
